package za.ac.sun.cs.distrib;

import gov.nasa.jpf.Config;
import gov.nasa.jpf.JPF;

public class Explorer {

	private static final String JPF_FILE = "src/examples/Test00.jpf";
	
	private static Config config;

	private static JPF jpf = null;

	public static void main(String[] args) {
		String[] configArgs = new String[1];
		if ((args.length > 0) && args[0].endsWith(".jpf")) {
			configArgs[0] = args[0];
		} else {
			configArgs[0] = JPF_FILE;
		}
		config = JPF.createConfig(configArgs);
		config.remove("listener");
		config.setProperty("search.class", "za.ac.sun.cs.distrib.TreeSearch");
		config.setProperty("search.TreeListener.redis.host", "localhost");
		config.setProperty("search.TreeListener.redis.port", "7777");
		config.setProperty("listener", "");
		config.setProperty("report.console.constraint", "");
//		config.printEntries();
		jpf = new JPF(config);
		jpf.run();
	}

}
